T:Type, L1,L2:(T List). (L1 = L2)  sublist(T; L1; L2) 

latex

Definitions	suptype(S; T), subtype(S; T), , True, T, prop{i:l}, False, A, A  B, lelt(i; j; k), t  T, P  Q, int_seg(i; j), x:A. B(x), sublist(T; L1; L2), P  Q, x:A. B(x)
Lemmas	nat wf, non neg length, increasing wf, squash wf, select wf, int seg wf, le wf, length wf1, id increasing